Nuprl Definition : msga
0,22
postcript
pdf
MsgA
==
ds
:
x
:Id fp
Type
==
da
:
a
:Knd fp
Type
==
x
:Id fp
ds
(
x
)?Void
==
a
:Id fp
State(
ds
)
Valtype(
da
;locl(
a
))
Prop
==
kx
:Knd
Id fp
State(
ds
)
Valtype(
da
;1of(
kx
))
ds
(2of(
kx
))?Void
==
kl
:Knd
IdLnk fp
(
tg
:Id
(State(
ds
)
Valtype(
da
;1of(
kl
))
(
da
(rcv(2of(
kl
),
tg
))?Void List))) List
==
x
:Id fp
Knd List
==
ltg
:IdLnk
Id fp
Knd List
==
k
:Knd fp
Id List
==
k
:Knd fp
IdLnk List
==
x
:Id fp
Knd List
==
Top
latex
clarification:
msga{i:l}
==
ds
:
x
:Id fp
Type{i}
==
da
:
a
:Knd fp
Type{i}
==
x
:Id fp
fpf-cap(
ds
;IdDeq;
x
;Void)
==
a
:Id fp
State(
ds
)
Valtype(
da
;locl(
a
))
Prop{i}
==
kx
:Knd
Id fp
State(
ds
)
Valtype(
da
;1of(
kx
))
fpf-cap(
ds
;IdDeq;2of(
kx
);Void)
==
kl
:Knd
IdLnk fp
==
(
tg
:Id
(State(
ds
)
Valtype(
da
;1of(
kl
))
(fpf-cap(
da
;KindDeq;rcv(2of(
kl
),
tg
);Void) List))) List
==
x
:Id fp
Knd List
==
ltg
:IdLnk
Id fp
Knd List
==
k
:Knd fp
Id List
==
k
:Knd fp
IdLnk List
==
x
:Id fp
Knd List
==
Top
latex
Definitions
Type
,
locl(
a
)
,
Prop
,
IdDeq
,
State(
ds
)
,
x
:
A
B
(
x
)
,
Valtype(
da
;
k
)
,
1of(
t
)
,
f
(
x
)?
z
,
KindDeq
,
rcv(
l
,
tg
)
,
2of(
t
)
,
Void
,
IdLnk
,
x
:
A
B
(
x
)
,
a
:
A
fp
B
(
a
)
,
Id
,
type
List
,
Knd
,
Top
FDL editor aliases
msga
origin